(declare-fun a () String)
(assert (and (= 0 (ite (= "\u{a}" (str.at (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len (str.substr a 1 (- (str.len a) 1))) 1)) 0)) 1 0)) (not (= (< 0 (str.len a)) (not (= 0 (ite (= "" a) 1 0))))) (= 0 (ite (= 0 (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len (str.substr a 1 (- (str.len a) 1))) 1)))) 1 0)) (> (str.len (str.substr a 1 (str.len (str.at (str.substr a 1 (- (str.len a) 1)) 0)))) 0) (not (= (and (not (= 0 (ite (= "" a) 1 0))) (= 0 (ite (= "" (str.at (str.substr (str.substr a 1 (str.len a)) 0 (- (str.len (str.substr a 0 (- (str.len a) 1))) 1)) 0)) 1 0))) (not (= 0 (ite (= "\u{a}" (str.at (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len (str.substr a 1 (- (str.len a) 1))) 1)) (- (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len (str.substr a 1 (- (str.len a) 1))) 1))) 1))) 1 0)))))))
(check-sat)
